n:, a, b:. sum(a+bi | i < n) = ((n(a+a+b(n-1)))  2) 

latex

Definitions	P  Q, P & Q, P  Q, , P  Q, Dec(P), Prop, a  b, , {i..j}, x. t(x), t  T, x:A. B(x), , sum(f(x) | x < k), P  Q, False, A, AB
Lemmas	nat wf, sum arith1, mul cancel in eq, sum wf, int seg wf, divide wfa, nequal wf, div rem sum, decidable le, rem invariant, le wf, rem 2 to 1